A, B, C:Realizer. A  B  B  C  A  C 

latex

Definitions	P  Q, i  j , False, A, A  B, {T}, SQType(T), ff, tt, P & Q, True, if b then t else f fi , Y, , t  T, A  B, P  Q, x:A. B(x), Rplus?(x1), b, , P  Q, Unit, , ,
Lemmas	Rnone?-implies, ge wf, nat properties, Rplus-right wf, Rplus-left wf, R-size-decreases, Rplus? wf, bool sq, bool cases, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf, Rnone? wf, le wf, es realizer wf, R-sub wf, nat plus wf, R-size wf, nat wf